Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    sel(s(X),cons(Y,Z))  → sel(X,activate(Z))
2:    sel(0,cons(X,Z))  → X
3:    first(0,Z)  → nil
4:    first(s(X),cons(Y,Z))  → cons(Y,n__first(X,activate(Z)))
5:    from(X)  → cons(X,n__from(s(X)))
6:    sel1(s(X),cons(Y,Z))  → sel1(X,activate(Z))
7:    sel1(0,cons(X,Z))  → quote(X)
8:    first1(0,Z)  → nil1
9:    first1(s(X),cons(Y,Z))  → cons1(quote(Y),first1(X,activate(Z)))
10:    quote(n__0)  → 01
11:    quote1(n__cons(X,Z))  → cons1(quote(activate(X)),quote1(activate(Z)))
12:    quote1(n__nil)  → nil1
13:    quote(n__s(X))  → s1(quote(activate(X)))
14:    quote(n__sel(X,Z))  → sel1(activate(X),activate(Z))
15:    quote1(n__first(X,Z))  → first1(activate(X),activate(Z))
16:    unquote(01)  → 0
17:    unquote(s1(X))  → s(unquote(X))
18:    unquote1(nil1)  → nil
19:    unquote1(cons1(X,Z))  → fcons(unquote(X),unquote1(Z))
20:    fcons(X,Z)  → cons(X,Z)
21:    first(X1,X2)  → n__first(X1,X2)
22:    from(X)  → n__from(X)
23:    0  → n__0
24:    cons(X1,X2)  → n__cons(X1,X2)
25:    nil  → n__nil
26:    s(X)  → n__s(X)
27:    sel(X1,X2)  → n__sel(X1,X2)
28:    activate(n__first(X1,X2))  → first(X1,X2)
29:    activate(n__from(X))  → from(X)
30:    activate(n__0)  → 0
31:    activate(n__cons(X1,X2))  → cons(X1,X2)
32:    activate(n__nil)  → nil
33:    activate(n__s(X))  → s(X)
34:    activate(n__sel(X1,X2))  → sel(X1,X2)
35:    activate(X)  → X
There are 40 dependency pairs:
36:    SEL(s(X),cons(Y,Z))  → SEL(X,activate(Z))
37:    SEL(s(X),cons(Y,Z))  → ACTIVATE(Z)
38:    FIRST(0,Z)  → NIL
39:    FIRST(s(X),cons(Y,Z))  → CONS(Y,n__first(X,activate(Z)))
40:    FIRST(s(X),cons(Y,Z))  → ACTIVATE(Z)
41:    FROM(X)  → CONS(X,n__from(s(X)))
42:    FROM(X)  → S(X)
43:    SEL1(s(X),cons(Y,Z))  → SEL1(X,activate(Z))
44:    SEL1(s(X),cons(Y,Z))  → ACTIVATE(Z)
45:    SEL1(0,cons(X,Z))  → QUOTE(X)
46:    FIRST1(s(X),cons(Y,Z))  → QUOTE(Y)
47:    FIRST1(s(X),cons(Y,Z))  → FIRST1(X,activate(Z))
48:    FIRST1(s(X),cons(Y,Z))  → ACTIVATE(Z)
49:    QUOTE1(n__cons(X,Z))  → QUOTE(activate(X))
50:    QUOTE1(n__cons(X,Z))  → ACTIVATE(X)
51:    QUOTE1(n__cons(X,Z))  → QUOTE1(activate(Z))
52:    QUOTE1(n__cons(X,Z))  → ACTIVATE(Z)
53:    QUOTE(n__s(X))  → QUOTE(activate(X))
54:    QUOTE(n__s(X))  → ACTIVATE(X)
55:    QUOTE(n__sel(X,Z))  → SEL1(activate(X),activate(Z))
56:    QUOTE(n__sel(X,Z))  → ACTIVATE(X)
57:    QUOTE(n__sel(X,Z))  → ACTIVATE(Z)
58:    QUOTE1(n__first(X,Z))  → FIRST1(activate(X),activate(Z))
59:    QUOTE1(n__first(X,Z))  → ACTIVATE(X)
60:    QUOTE1(n__first(X,Z))  → ACTIVATE(Z)
61:    UNQUOTE(01)  → 0#
62:    UNQUOTE(s1(X))  → S(unquote(X))
63:    UNQUOTE(s1(X))  → UNQUOTE(X)
64:    UNQUOTE1(nil1)  → NIL
65:    UNQUOTE1(cons1(X,Z))  → FCONS(unquote(X),unquote1(Z))
66:    UNQUOTE1(cons1(X,Z))  → UNQUOTE(X)
67:    UNQUOTE1(cons1(X,Z))  → UNQUOTE1(Z)
68:    FCONS(X,Z)  → CONS(X,Z)
69:    ACTIVATE(n__first(X1,X2))  → FIRST(X1,X2)
70:    ACTIVATE(n__from(X))  → FROM(X)
71:    ACTIVATE(n__0)  → 0#
72:    ACTIVATE(n__cons(X1,X2))  → CONS(X1,X2)
73:    ACTIVATE(n__nil)  → NIL
74:    ACTIVATE(n__s(X))  → S(X)
75:    ACTIVATE(n__sel(X1,X2))  → SEL(X1,X2)
The approximated dependency graph contains 6 SCCs: {36,37,40,69,75}, {43,45,53,55}, {47}, {51}, {63} and {67}.
Tyrolean Termination Tool  (0.65 seconds)   ---  May 3, 2006